COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	
C00006 00003	We decided long ago that if such a ?f existed it must certainly be
C00013 00004	Now we investigate the possibility of completeness between deducibility
C00019 ENDMK
C⊗;


We've taken a slight side trip on our way to showing non-existence
of a decision procedure, ?f, for provability in ENT. We did not need the
result that any function representable in ENT is recursive to show
undecidability, but we will need it shortly when we look at completeness. Now
let's get back to the decision problem.

Recall the definition of πD(πu) ({yon(R11)}) and that πD is recursive.
Let ⊗T be the set of G⊗odel numbers of theorems of ENT.

%7THEOREM 16%1 If ENT is consistent and the function πD is representable in ENT,
then ⊗T is not expressible in ENT.

Proof:
.begin indent 10,10;
Assume πD is representable and ⊗T is expressible in ENT. Then there are wffs
?D(λx1,λx2) and  ?T(λx2) such that:
.begin indent 15,15;nofill
1) If πD(πk) = πj then ?ε?D(λk, λj)
2) (∃! λx2)?D(λk,λx2)
3) If πk is in ⊗T, then ?ε?T(λk)
4) If πk is not in ⊗T, then ?ε~?T(λk)
.end

Consider the formula: ?A(λx1): (∀λx2)(?D(λx1,λx2) ⊃ ?T(λx2)). Let
πp be the G⊗odel number of this wff. Construct the wff:
.begin center

?A(λp): (∀λx2)(?D(λp, λx2) ⊃ ~?T(λx2))
.end

Let πq be the G⊗odel number of ?A(λp). Hence πD(πp)#=#πq.
Therefore, by 1), ?ε?D(λp,λq). Now, either ?ε?A(λp) or not ?ε?A(λp).

If  not ?ε?A(λp), then πq is not in ⊗T and so by 4), ?ε~?T(λq).
On the other hand if ?ε?A(λp) then ?ε(∀λx2)(?D(λp,λx2)#⊃#~?T(λx2)).
Hence by Axiom 4, and ?MP
?ε?D(λp,λq)#⊃#~?T(λq); but
?ε?D(λp,λq). Hence
?ε~?T(λq).
Thus in both cases, ?ε~?T(λq).

Now from ?ε?D(λp,λq) and 2),
?ε?D(λp,λx2)#⊃#(λx2#=#λq).
But since ?ε~?T(λq),
?ελx2#=#λq#⊃#
~?T(λx2).
Hence ?ε?D(λp,λx2)#⊃#~?T(λx2), and by ?Gen,
?ε(∀λx2)(?D(λp,λx2)#⊃#~?T(λx2)), i.e. ?ε?A(λp).

Therefore πq is in ⊗T and by 3), ?ε?T(λq). 

Since we also have ?ε~?T(λq), ENT is inconsistent; a contradiction.
Therefore, under the given hypotheses, ⊗T is not expressible.
.end

%7Corollary 16.1%1 If ENT is consistent and every recursive function
is expressible in ENT, then ⊗T is not expressible in ENT. Hence ⊗T is not
recursive.

Proof:
.begin indent 10,10;
πD is recursive, and therefore representable. By theorem 16, ⊗T is not 
expressible. By lemma 10 ({yon(R5)}), the characteristic function
πC%4TO%1 is not recursive, and so, ⊗T is not recursive.
.end

We chose the notation ⊗T for our set of theorems because ?f is the 
characteristic function of ⊗T.  That is,
.begin nofill;

				π0 if ?Aε⊗T
		?f(?A) =
				π1 if ?A?N⊗T

.end
We decided long ago that if such a ?f existed it must certainly be
effectively computable, which by G⊗odel's work means that it must be
recursive.  Corollary 16.1 states that it is not recursive, thus we
conclude that it does not exist.

.begin center

Therefore ENT is undecidable.
.end
We mentioned earlier that undecidability for PC follows from this result.

.begin indent 0,10;
%7THEOREM 17%1 Let ⊗K1 and ⊗K2 be first-order theories having the same symbols
as ENT. If ⊗K2 is a finite extension of ⊗K1, and ⊗K2 is undecidable, then
⊗K1 is also undecidable.

.turn off "{","}";
Proof: Let ⊗A be a set of axioms of ⊗K1 and ⊗A∪{?A1,#...,#?An} be the set of
axioms for ⊗K2. We may assume ?A1,#...,#?An are closed wffs.
By the Deduction Theorem, a wff ?B is provable in ⊗K2 iff
(?A1∧?A2∧#...∧?An)⊃?B is provable in ⊗K1. Therefore if ⊗K1 were
decidable ⊗K2 would also be decidable. Thus ⊗K1 is undecidable.
.turn on "{","}";
.end
Thus if we can exhibit a finite extension of PC which is undecidable, we will
have shown PC itself is undecidable. First we will define precisely what we
mean by a finite extension, and also compatibility.

Let ⊗K1 and ⊗K2 be two first-order theories having the same symbols.
⊗K2 is called a %3⊗→finite extension↔←%1 of ⊗K1 iff there is a set ⊗A of wffs
and a %2finite%1 set ⊗B of wffs such that:
.begin indent 5,5;
1) the theorems of ⊗K1 are precisely the wffs derivable from ⊗A.

2) the theorems of ⊗K2 are precisely the wffs derivable from ⊗A∪⊗B.
.end
We say that ⊗K1 and ⊗K2 be are %3⊗→compatible↔←%1 iff the theory ⊗K1∪⊗K2, the set of
axioms of which is the union of the sets of axioms of ⊗K1 
and the set of axioms of ⊗K2, is consistent.

Unfortunately ENT is not a finite extension of PC since %7A14%1 is an axiom schema
by which we have added an infinite number of axioms. But we didn't need an infinite
number of axioms in the proof of undecidability. What we do need is "enough"
axioms to ensure that every recursive function is representable in our theory.

Raphael Robinson came up with such a system called "⊗→Robinson's System↔←" which we 
shall call ⊗→RR↔←.  RR is a first-order theory with the same symbols as ENT and having
the following finite number of proper axioms.
.begin nofill;indent 5;
1) λx1 = λx1
2) λx1 = λx2 ⊃ λx2 = λx1
3) λx1 = λx2 ⊃ (λx2 = λx3 ⊃ λx1 = λx3)
4) λx1 = λx2 ⊃ λx1' = λx2'
5) λx1 = λx2 ⊃ (λx1+λx3 = λx2+λx3 ∧ λx3+λx1 = λx3+λx2)
6) λx1 = λx2 ⊃ (λx1⊗xλx3 = λx2⊗xλx3 ∧ λx3⊗xλx1 = λx3⊗xλx2)
7) λx1' = λx2' ⊃ λx1 = λx2
8) λ0 ≠ λx1'
9) λx1 ≠ λ0 ⊃ (∃λx2)(λx1 = λx2')
10) λx1+λ0 = λx1
11) λx1+λx2' = (λx1+λx2)'
12) λx1⊗xλ0 = λ0
13) λx1⊗xλx2' = (λx1⊗xλx2)+λx1
.end

RR is a proper subtheory of ENT. It can be shown that 
every recursive function is representable in RR and that RR is undecidable.
It follows that PC is undecidable.

.group;
%7THEOREM 18%1 PC is undecidable.
.begin indent 0,10;
Proof: RR is a finite extension of PC. In the definition of  finite extension
the set ⊗A is the set of axioms for PC (%7A1-A5%1) and the set ⊗B is the set
of axioms 1)-13). Since RR is undecidable, PC must also be undecidable
by Theorem 17.
.end
.apart;
.GROUP
These results can be generalized further. In theorem 16 and corollary 16.1
we could replace "ENT" by any first-order theory "⊗K" with equality (i.e. a
substitutive equivalence relation). Thus we have:

%7Corollary 16.2%1 If ⊗K is consistent and every recursive function is
representable in ⊗K, then the set of theorems of ⊗K, %6T%4K%1, is not
expressible in ⊗K. Hence ⊗K is undecidable.
.apart

We say ⊗K is %3⊗→essentially undecidable↔←%1 iff ⊗K and every consistent extension of
⊗K is undecidable.

.group;
%7THEOREM 19%1 If ⊗K is consistent and every recursive function is 
representable in ⊗K, then ⊗K is essentially undecidable.
.BEGIN INDENT 0,10;
Proof: Let %6T%1 be any consistent extension of ⊗K. Since every
recursive function is representable in ⊗K the same holds for %6T%1, and therefore,
by corollary 16.2, %6T%1 is undecidable.
.end
.apart
Now we investigate the possibility of completeness between deducibility
and truth.

Recall the definition of πW1(πu, πy) on {yon (W1)}.
πW1(πu, πy) is primitive recursive and so by corollary 13.1 πW1 is
expressible in ENT by a wff λW1(λx1,λx2) with two free variables λx1, λx2,
i.e., if πW1(πk1, πk2), then ?ελW1(λk1, λk2), and if not-πW1(πk1, πk2),
then ?ε~λW1(λk1, λk2).  Consider the wff
.begin center;

(*)  (∀λx2)~λW1(λx1, λx2)
.end

Let πm be the G⊗odel number of the wff (*). Substitute λm for λx1 in (*) to obtain
the closed wff:
.begin center;

(**)  (∀λx2)~λW1(λm, λx2)
.end
Recall that πW1(πu,#πy) holds iff πu is the G⊗odel number
of a wff ?A(λx1) containing the free variable λx1, and πy is the G⊗odel
number of a proof in ENT of ?A(λu). Now πm is the G⊗odel number of (*), and
(**) comes from (*) by substituting λm for the variable λx1. Hence:
.BEGIN  CENTER;
(I) πW1(πm,πy) holds iff πy is the G⊗odel number of a proof in ENT of (**).
.end

Recall the definition of ?w-consistency: for every wff, ?A(?x), if
?ε?A(λn) for every natural number πn, then it is not the case that ?ε(∃λx)~?A(λx).

.BEGIN GROUP;
%7THEOREM 20%1 (G⊗odel's theorem for ENT)
.INDENT 10,10;
1)If ENT is consistent, then the wff (**) is not provable in ENT.

2) If ENT is ?w-consistent, then the wff ~(**) is not provable in ENT.

.indent 0,10;
Proof: 

1) Assume ENT is consistent, and assume that
?ε (∀λx2)~λW1(λm, λx2). Let πk be the G⊗odel number of a proof of this
wff.  By (I) above, πW1(πm,#πk). Since λW1 expresses πW1 in ENT, we have 
?ελW1(λm,#λk). From
?ε (∀λx2)~λW1(λm, λx2), by %7A4%1 and ?MP we can deduce 
~λW1(λm,λk). Thus
~λW1(λm,λk) and
λW1(λm,λk) are both provable. This obviously contradicts the consistency of ENT.

2) Assume ENT is ?w-consistent, and assume that
?ε#~(∀λx2)~λW1(λm, λx2); i.e. ?ε~(**).  By the Remark on {yon(R6)} ENT is consistent,
so we know not-?ε(**). Therefore, for every natural number πn, πn is not the G⊗odel number
of a proof in ENT of (**), i.e., by (I), for every πn, πW1(πm, πn) is false.  So
for every πn, ?ε~λW1(λm,#λn).  If we let ?A(λx2) be ~λW1(λm,#λx2), then, by the
?w-consistency of ENT, it follows that not-?ε(∃λx2)~~λW1(λm,#λx2), hence
not-?ε(∃λx2)λW1(λm,#λx2).  But this contradicts our assumption that 
?ε(∃λx2)λW1(λm,#λx2).
.end

Hence, if ENT is  ?w-consistent, the closed wff (**) is neither provable nor
disprovable in ENT.  Such a closed wff is said to be an ⊗→undecidable sentence↔← of 
ENT.  The standard interpretation of the undecidable sentence (**):
(∀λx2)~λW1(λm,#λx2) is worth mentioning.  Since λW1 expresses the relation πW1
in ENT, (**) states that πW1(πm,#πx2) is false for every natural number πx2.  By
(I), this means that there is no proof in ENT of (**).  In other words, (**)
is a statement which declares its own unprovability.  Now, by G⊗odel's theorem,
if ENT is consistent, then (**) is, in fact, unprovable, and therefore is a
true statement under the standard interpretation.  So we have a statement
which is true but not provable.

G⊗odel's theorem involves the assumption of ?w-consistency, but, at the cost
of complicating the argument, we need only consistency (see Mendelson [8]).

We have not shown rigorously that every statement provable in ENT is in
fact true.  This should be clear as the proof of the same for PC will
suffice, with the addition that the axioms %7A6-A14%1 are indeed true.  We
take this as obvious due to the remarks in {yonss (R4)}.